(0) Obligation:
Clauses:
preorder(X, Y) :- pdl(X, -(Y, [])).
pdl(nil, Y) :- ','(!, eq(Y, -(X, X))).
pdl(T, -(.(X, Xs), Zs)) :- ','(value(T, X), ','(left(T, L), ','(right(T, R), ','(pdl(L, -(Xs, Ys)), pdl(R, -(Ys, Zs)))))).
left(nil, nil).
left(tree(L, X1, X2), L).
right(nil, nil).
right(tree(X3, X4, R), R).
value(nil, X5).
value(tree(X6, X, X7), X).
eq(X, X).
Query: preorder(g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
pdlA(tree(X1, X2, X3), .(X2, X4)) :- pdlB(X1, X4, X5).
pdlA(tree(X1, X2, X3), .(X2, X4)) :- ','(pdlcB(X1, X4, X5), pdlA(X3, X5)).
pdlB(tree(X1, X2, X3), .(X2, X4), X5) :- pdlB(X1, X4, X6).
pdlB(tree(X1, X2, X3), .(X2, X4), X5) :- ','(pdlcB(X1, X4, X6), pdlB(X3, X6, X5)).
preorderC(X1, X2) :- pdlA(X1, X2).
Clauses:
pdlcA(nil, []).
pdlcA(tree(X1, X2, X3), .(X2, X4)) :- ','(pdlcB(X1, X4, X5), pdlcA(X3, X5)).
pdlcB(nil, X1, X1).
pdlcB(tree(X1, X2, X3), .(X2, X4), X5) :- ','(pdlcB(X1, X4, X6), pdlcB(X3, X6, X5)).
Afs:
preorderC(x1, x2) = preorderC(x1)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
preorderC_in: (b,f)
pdlA_in: (b,f)
pdlB_in: (b,f,f)
pdlcB_in: (b,f,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
PREORDERC_IN_GA(X1, X2) → U7_GA(X1, X2, pdlA_in_ga(X1, X2))
PREORDERC_IN_GA(X1, X2) → PDLA_IN_GA(X1, X2)
PDLA_IN_GA(tree(X1, X2, X3), .(X2, X4)) → U1_GA(X1, X2, X3, X4, pdlB_in_gaa(X1, X4, X5))
PDLA_IN_GA(tree(X1, X2, X3), .(X2, X4)) → PDLB_IN_GAA(X1, X4, X5)
PDLB_IN_GAA(tree(X1, X2, X3), .(X2, X4), X5) → U4_GAA(X1, X2, X3, X4, X5, pdlB_in_gaa(X1, X4, X6))
PDLB_IN_GAA(tree(X1, X2, X3), .(X2, X4), X5) → PDLB_IN_GAA(X1, X4, X6)
PDLB_IN_GAA(tree(X1, X2, X3), .(X2, X4), X5) → U5_GAA(X1, X2, X3, X4, X5, pdlcB_in_gaa(X1, X4, X6))
U5_GAA(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → U6_GAA(X1, X2, X3, X4, X5, pdlB_in_gaa(X3, X6, X5))
U5_GAA(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → PDLB_IN_GAA(X3, X6, X5)
PDLA_IN_GA(tree(X1, X2, X3), .(X2, X4)) → U2_GA(X1, X2, X3, X4, pdlcB_in_gaa(X1, X4, X5))
U2_GA(X1, X2, X3, X4, pdlcB_out_gaa(X1, X4, X5)) → U3_GA(X1, X2, X3, X4, pdlA_in_ga(X3, X5))
U2_GA(X1, X2, X3, X4, pdlcB_out_gaa(X1, X4, X5)) → PDLA_IN_GA(X3, X5)
The TRS R consists of the following rules:
pdlcB_in_gaa(nil, X1, X1) → pdlcB_out_gaa(nil, X1, X1)
pdlcB_in_gaa(tree(X1, X2, X3), .(X2, X4), X5) → U11_gaa(X1, X2, X3, X4, X5, pdlcB_in_gaa(X1, X4, X6))
U11_gaa(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → U12_gaa(X1, X2, X3, X4, X5, X6, pdlcB_in_gaa(X3, X6, X5))
U12_gaa(X1, X2, X3, X4, X5, X6, pdlcB_out_gaa(X3, X6, X5)) → pdlcB_out_gaa(tree(X1, X2, X3), .(X2, X4), X5)
The argument filtering Pi contains the following mapping:
pdlA_in_ga(
x1,
x2) =
pdlA_in_ga(
x1)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
pdlB_in_gaa(
x1,
x2,
x3) =
pdlB_in_gaa(
x1)
pdlcB_in_gaa(
x1,
x2,
x3) =
pdlcB_in_gaa(
x1)
nil =
nil
pdlcB_out_gaa(
x1,
x2,
x3) =
pdlcB_out_gaa(
x1)
U11_gaa(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gaa(
x1,
x2,
x3,
x6)
U12_gaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U12_gaa(
x1,
x2,
x3,
x7)
PREORDERC_IN_GA(
x1,
x2) =
PREORDERC_IN_GA(
x1)
U7_GA(
x1,
x2,
x3) =
U7_GA(
x1,
x3)
PDLA_IN_GA(
x1,
x2) =
PDLA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x1,
x2,
x3,
x5)
PDLB_IN_GAA(
x1,
x2,
x3) =
PDLB_IN_GAA(
x1)
U4_GAA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GAA(
x1,
x2,
x3,
x6)
U5_GAA(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GAA(
x1,
x2,
x3,
x6)
U6_GAA(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_GAA(
x1,
x2,
x3,
x6)
U2_GA(
x1,
x2,
x3,
x4,
x5) =
U2_GA(
x1,
x2,
x3,
x5)
U3_GA(
x1,
x2,
x3,
x4,
x5) =
U3_GA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PREORDERC_IN_GA(X1, X2) → U7_GA(X1, X2, pdlA_in_ga(X1, X2))
PREORDERC_IN_GA(X1, X2) → PDLA_IN_GA(X1, X2)
PDLA_IN_GA(tree(X1, X2, X3), .(X2, X4)) → U1_GA(X1, X2, X3, X4, pdlB_in_gaa(X1, X4, X5))
PDLA_IN_GA(tree(X1, X2, X3), .(X2, X4)) → PDLB_IN_GAA(X1, X4, X5)
PDLB_IN_GAA(tree(X1, X2, X3), .(X2, X4), X5) → U4_GAA(X1, X2, X3, X4, X5, pdlB_in_gaa(X1, X4, X6))
PDLB_IN_GAA(tree(X1, X2, X3), .(X2, X4), X5) → PDLB_IN_GAA(X1, X4, X6)
PDLB_IN_GAA(tree(X1, X2, X3), .(X2, X4), X5) → U5_GAA(X1, X2, X3, X4, X5, pdlcB_in_gaa(X1, X4, X6))
U5_GAA(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → U6_GAA(X1, X2, X3, X4, X5, pdlB_in_gaa(X3, X6, X5))
U5_GAA(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → PDLB_IN_GAA(X3, X6, X5)
PDLA_IN_GA(tree(X1, X2, X3), .(X2, X4)) → U2_GA(X1, X2, X3, X4, pdlcB_in_gaa(X1, X4, X5))
U2_GA(X1, X2, X3, X4, pdlcB_out_gaa(X1, X4, X5)) → U3_GA(X1, X2, X3, X4, pdlA_in_ga(X3, X5))
U2_GA(X1, X2, X3, X4, pdlcB_out_gaa(X1, X4, X5)) → PDLA_IN_GA(X3, X5)
The TRS R consists of the following rules:
pdlcB_in_gaa(nil, X1, X1) → pdlcB_out_gaa(nil, X1, X1)
pdlcB_in_gaa(tree(X1, X2, X3), .(X2, X4), X5) → U11_gaa(X1, X2, X3, X4, X5, pdlcB_in_gaa(X1, X4, X6))
U11_gaa(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → U12_gaa(X1, X2, X3, X4, X5, X6, pdlcB_in_gaa(X3, X6, X5))
U12_gaa(X1, X2, X3, X4, X5, X6, pdlcB_out_gaa(X3, X6, X5)) → pdlcB_out_gaa(tree(X1, X2, X3), .(X2, X4), X5)
The argument filtering Pi contains the following mapping:
pdlA_in_ga(
x1,
x2) =
pdlA_in_ga(
x1)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
pdlB_in_gaa(
x1,
x2,
x3) =
pdlB_in_gaa(
x1)
pdlcB_in_gaa(
x1,
x2,
x3) =
pdlcB_in_gaa(
x1)
nil =
nil
pdlcB_out_gaa(
x1,
x2,
x3) =
pdlcB_out_gaa(
x1)
U11_gaa(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gaa(
x1,
x2,
x3,
x6)
U12_gaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U12_gaa(
x1,
x2,
x3,
x7)
PREORDERC_IN_GA(
x1,
x2) =
PREORDERC_IN_GA(
x1)
U7_GA(
x1,
x2,
x3) =
U7_GA(
x1,
x3)
PDLA_IN_GA(
x1,
x2) =
PDLA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x1,
x2,
x3,
x5)
PDLB_IN_GAA(
x1,
x2,
x3) =
PDLB_IN_GAA(
x1)
U4_GAA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GAA(
x1,
x2,
x3,
x6)
U5_GAA(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GAA(
x1,
x2,
x3,
x6)
U6_GAA(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_GAA(
x1,
x2,
x3,
x6)
U2_GA(
x1,
x2,
x3,
x4,
x5) =
U2_GA(
x1,
x2,
x3,
x5)
U3_GA(
x1,
x2,
x3,
x4,
x5) =
U3_GA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PDLB_IN_GAA(tree(X1, X2, X3), .(X2, X4), X5) → U5_GAA(X1, X2, X3, X4, X5, pdlcB_in_gaa(X1, X4, X6))
U5_GAA(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → PDLB_IN_GAA(X3, X6, X5)
PDLB_IN_GAA(tree(X1, X2, X3), .(X2, X4), X5) → PDLB_IN_GAA(X1, X4, X6)
The TRS R consists of the following rules:
pdlcB_in_gaa(nil, X1, X1) → pdlcB_out_gaa(nil, X1, X1)
pdlcB_in_gaa(tree(X1, X2, X3), .(X2, X4), X5) → U11_gaa(X1, X2, X3, X4, X5, pdlcB_in_gaa(X1, X4, X6))
U11_gaa(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → U12_gaa(X1, X2, X3, X4, X5, X6, pdlcB_in_gaa(X3, X6, X5))
U12_gaa(X1, X2, X3, X4, X5, X6, pdlcB_out_gaa(X3, X6, X5)) → pdlcB_out_gaa(tree(X1, X2, X3), .(X2, X4), X5)
The argument filtering Pi contains the following mapping:
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
pdlcB_in_gaa(
x1,
x2,
x3) =
pdlcB_in_gaa(
x1)
nil =
nil
pdlcB_out_gaa(
x1,
x2,
x3) =
pdlcB_out_gaa(
x1)
U11_gaa(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gaa(
x1,
x2,
x3,
x6)
U12_gaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U12_gaa(
x1,
x2,
x3,
x7)
PDLB_IN_GAA(
x1,
x2,
x3) =
PDLB_IN_GAA(
x1)
U5_GAA(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GAA(
x1,
x2,
x3,
x6)
We have to consider all (P,R,Pi)-chains
(8) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PDLB_IN_GAA(tree(X1, X2, X3)) → U5_GAA(X1, X2, X3, pdlcB_in_gaa(X1))
U5_GAA(X1, X2, X3, pdlcB_out_gaa(X1)) → PDLB_IN_GAA(X3)
PDLB_IN_GAA(tree(X1, X2, X3)) → PDLB_IN_GAA(X1)
The TRS R consists of the following rules:
pdlcB_in_gaa(nil) → pdlcB_out_gaa(nil)
pdlcB_in_gaa(tree(X1, X2, X3)) → U11_gaa(X1, X2, X3, pdlcB_in_gaa(X1))
U11_gaa(X1, X2, X3, pdlcB_out_gaa(X1)) → U12_gaa(X1, X2, X3, pdlcB_in_gaa(X3))
U12_gaa(X1, X2, X3, pdlcB_out_gaa(X3)) → pdlcB_out_gaa(tree(X1, X2, X3))
The set Q consists of the following terms:
pdlcB_in_gaa(x0)
U11_gaa(x0, x1, x2, x3)
U12_gaa(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(10) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- U5_GAA(X1, X2, X3, pdlcB_out_gaa(X1)) → PDLB_IN_GAA(X3)
The graph contains the following edges 3 >= 1
- PDLB_IN_GAA(tree(X1, X2, X3)) → PDLB_IN_GAA(X1)
The graph contains the following edges 1 > 1
- PDLB_IN_GAA(tree(X1, X2, X3)) → U5_GAA(X1, X2, X3, pdlcB_in_gaa(X1))
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3
(11) YES
(12) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PDLA_IN_GA(tree(X1, X2, X3), .(X2, X4)) → U2_GA(X1, X2, X3, X4, pdlcB_in_gaa(X1, X4, X5))
U2_GA(X1, X2, X3, X4, pdlcB_out_gaa(X1, X4, X5)) → PDLA_IN_GA(X3, X5)
The TRS R consists of the following rules:
pdlcB_in_gaa(nil, X1, X1) → pdlcB_out_gaa(nil, X1, X1)
pdlcB_in_gaa(tree(X1, X2, X3), .(X2, X4), X5) → U11_gaa(X1, X2, X3, X4, X5, pdlcB_in_gaa(X1, X4, X6))
U11_gaa(X1, X2, X3, X4, X5, pdlcB_out_gaa(X1, X4, X6)) → U12_gaa(X1, X2, X3, X4, X5, X6, pdlcB_in_gaa(X3, X6, X5))
U12_gaa(X1, X2, X3, X4, X5, X6, pdlcB_out_gaa(X3, X6, X5)) → pdlcB_out_gaa(tree(X1, X2, X3), .(X2, X4), X5)
The argument filtering Pi contains the following mapping:
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
pdlcB_in_gaa(
x1,
x2,
x3) =
pdlcB_in_gaa(
x1)
nil =
nil
pdlcB_out_gaa(
x1,
x2,
x3) =
pdlcB_out_gaa(
x1)
U11_gaa(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_gaa(
x1,
x2,
x3,
x6)
U12_gaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U12_gaa(
x1,
x2,
x3,
x7)
PDLA_IN_GA(
x1,
x2) =
PDLA_IN_GA(
x1)
U2_GA(
x1,
x2,
x3,
x4,
x5) =
U2_GA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(13) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PDLA_IN_GA(tree(X1, X2, X3)) → U2_GA(X1, X2, X3, pdlcB_in_gaa(X1))
U2_GA(X1, X2, X3, pdlcB_out_gaa(X1)) → PDLA_IN_GA(X3)
The TRS R consists of the following rules:
pdlcB_in_gaa(nil) → pdlcB_out_gaa(nil)
pdlcB_in_gaa(tree(X1, X2, X3)) → U11_gaa(X1, X2, X3, pdlcB_in_gaa(X1))
U11_gaa(X1, X2, X3, pdlcB_out_gaa(X1)) → U12_gaa(X1, X2, X3, pdlcB_in_gaa(X3))
U12_gaa(X1, X2, X3, pdlcB_out_gaa(X3)) → pdlcB_out_gaa(tree(X1, X2, X3))
The set Q consists of the following terms:
pdlcB_in_gaa(x0)
U11_gaa(x0, x1, x2, x3)
U12_gaa(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(15) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- U2_GA(X1, X2, X3, pdlcB_out_gaa(X1)) → PDLA_IN_GA(X3)
The graph contains the following edges 3 >= 1
- PDLA_IN_GA(tree(X1, X2, X3)) → U2_GA(X1, X2, X3, pdlcB_in_gaa(X1))
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3
(16) YES